#include "utilities.hh"
#include "cuddInt.h"

BDD xorlist(vector<BDD> *bddlist)
{
    // This function returns a BDD that is true iff only one condition
    // of the list is true. E.g., if the list is {a,b,c},
    // xorlist(a,b,c) = (a and !b and !c)or(!a and b and !c)or(!a and !b and c)
    // NOTICE: This is not the standard meaning of xor!
    vector<BDD>::iterator bddi;

    int i = 0;

    BDD result = bddmgr->bddZero();

    if (bddlist->size() < 1)
        return result;

    BDD tmpres = bddmgr->bddOne();

    int j = 0;

    for (i = 0; i < (int) bddlist->size(); i++)
    {
        for (bddi = bddlist->begin(); bddi != bddlist->end(); bddi++)
        {
            if (j == i)
            {
                tmpres = tmpres * (*bddi);
            }
            else
            {
                tmpres = tmpres * !(*bddi);
            }
            j++;
        }
        result = result + tmpres;
        tmpres = bddmgr->bddOne();
        j = 0;
    }

    return result;
}

BDD Exists(BDDvector* v, BDD x)
{
    BDD tmp = bddmgr->bddOne(); // Always true

    for (int j = 0; j < v->count(); j++)
    {
        tmp = tmp * (*v)[j];
    }

    return x.ExistAbstract(tmp);
}

ADD ADDExists(ADDvector v, ADD x)
{
    ADD tmp = bddmgr->addOne(); // Always true

    for (int j = 0; j < v.count(); j++)
    {
        tmp = tmp * v[j];
    }
    return x.ExistAbstract(tmp);
}

BDD timesTrans(BDD *from, BDD *to)
{
    BDD result;
    if (options["experiment"] == 0)
    {
        result = (*from) * (*to) * preRT * andprot;
    }
    else
    {
        result = (*from) * (*to) * (*vRT)[0];
        for (unsigned int i = 1; i < agents->size(); i++)
            result *= (*vRT)[i];
    }
    return result;
}

BDD timesRT(BDD *state)
{
    BDD result;
    if (options["experiment"] == 0)
    {
        result = (*state) * RT;
    }
    else
    {
        result = (*state) * (*vRT)[0];
        for (unsigned int i = 1; i < agents->size(); i++)
            result *= (*vRT)[i];
        result = Exists(a, result);
    }
    return result;
}

BDD check_EX_new(BDD next)
{
    // Computes the preimage
    if ((options["bddcache"] == 1 || options["bddcache"] == 3) && calReachRT)
    {
        reachRT = reach;
        for (unsigned int i = 0; i < agents->size(); i++)
            reachRT *= (*vRT)[i];
        calReachRT = false;
    }
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    if (options["bddcache"] == 1 || options["bddcache"] == 3)
    {
        BDD result = next * reachRT;
        result = Exists(pv, result); // States from which...
        result = Exists(a, result); //Exists a joint action...
        return result * reach;
    }
    else
    {
        BDD result = next * reach;
        for (unsigned int i = 0; i < agents->size(); i++)
            result *= (*vRT)[i];
        result = Exists(pv, result); // States from which...
        result = Exists(a, result); //Exists a joint action...
        return result * reach;
    }

}

BDD check_EX(BDD next)
{
    if (options["experiment"] >= 1)
        return check_EX_new(next);
    // Computes the preimage
    if ((options["bddcache"] == 1 || options["bddcache"] == 3) && calReachRT)
    {
        reachRT = RT * reach * andprot;
        calReachRT = false;
    }
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result =
            (options["bddcache"] == 1 || options["bddcache"] == 3) ? Exists(pv,
                    next * reachRT) : Exists(pv, RT * next * reach * andprot); // States from which...
    result = Exists(a, result * andprot); //Exists a joint action...
    return result * reach;

}

BDD check_EF(BDD p)
{
    // Computes the fixpoint iterating false
    BDD tmp = bddmgr->bddOne();
    BDD q = bddmgr->bddZero();
    while (q != tmp)
    {
        tmp = q;
        q = p + check_EX(tmp);
    }
    return q * reach;
}

BDD check_EG(BDD p)
{
    // Computes the fixpoint iterating false
    BDD tmp = bddmgr->bddZero();
    BDD q = bddmgr->bddOne();
    while (q != tmp)
    {
        tmp = q;
        q = p * check_EX(tmp);
    }
    return q;
}

BDD check_EU(BDD p, BDD q)
{ // See Huth-Ryan, pag. 180
    BDD W = p;
    BDD X = reach;
    BDD Y = q;
    while (X != Y)
    {
        X = Y;
        //cout << "check_EX(Y): ";
        //check_EX(Y).print(v->count(), 2);
        Y = Y + (W * check_EX(Y));
    }
    return Y;
}

BDD check_AU(BDD p, BDD q)
{// Tricky one, see Huth Ryan pag. 167 and 179
    // A(p U q) = !(E(!q U (!p * !q) ) + EG(!q))
    // For weak until, see page 202 Huth-Ryan
    BDD result;
    // Weak until:
    //result = !(check_EU(!q,!(p + q))) ;

    result = !(check_EU(!q, !(p * q)) + check_EG(!q)) * reach;
    return result;
}

BDD check_nK(BDD next, BDD RK)
{
    // Used for K and GK and GCK
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RK * next * reach); // States from which...
    //result = Exists(a,result*andprot,bddmgr); //Exists a joint action...
    return result;
}

BDD check_nO(BDD next, BDD RO)
{
    // Check deontic
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RO * next * reach); // States from which...
    //result = Exists(a,result*andprot); //Exists a joint action...
    return result;
}

BDD check_nKH(BDD next, BDD RK, BDD RO)
{
    // Check knowledge assyming correct behaviour
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RO * RK * next * reach); // States from which...
    //result = Exists(a,result*andprot); //Exists a joint action...
    return result;
}

BDD check_GK(BDD next, BDD RK)
{
    //cout << "IN GK" << endl;
    //next.print(2,2);
    //RK.print(2,2);

    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RK * !next * reach); // States from which...
    //result = Exists(a,result*andprot); //Exists a joint action...
    result = !result * reach;
    //result.print(2,2);
    return result;
}

BDD check_nGK(BDD next, BDD RK)
{
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RK * next * reach); // States from which...
    return result;
}

BDD check_DK(BDD next, BDD RK)
{
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RK * !next * reach); // States from which...
    //result = Exists(a,result*andprot); //Exists a joint action...
    result = !result * reach;
    return result;
}

BDD check_nDK(BDD next, BDD RK)
{
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RK * next * reach); // States from which...
    return result;
}

BDD check_GCK(BDD next, BDD RK)
{
    // GCK p = GK(p * GCK(p)) see fhmv:rak, section 11.5
    // cout << "In GCK, formula to be checked:" << endl;
    //next.print(2,2);
    //cout << "relation:" << endl;
    //RK.print(2,2);

    BDD tmp = reach;
    BDD tmp2 = next;

    if ((options["bddcache"] == 1 || options["bddcache"] == 3))
    {
        BDD reachRK = reach * RK;
        while (tmp != tmp2)
        {
            tmp2 = tmp;
            tmp = (next * tmp).SwapVariables(*v, *pv);
            tmp = (!Exists(pv, reachRK * !tmp)) * reach;
        }
    }
    else
    {
        while (tmp != tmp2)
        {
            tmp2 = tmp;
            tmp = check_GK(next * tmp, RK);
        }
    }
    //cout << "result in GCK " << i;
    //tmp.print(2,2);
    return tmp;
}

BDD check_GCK_new(BDD next, string name)
{
    // GCK p = GK(p * GCK(p)) see fhmv:rak, section 11.5
    // cout << "In GCK, formula to be checked:" << endl;
    //next.print(2,2);
    //cout << "relation:" << endl;
    //RK.print(2,2);

    BDD tmp = reach;
    BDD tmp2 = next;
    map<string, set<string> >::iterator gi = is_groups->find(name);
    BDD swapreach = reach.SwapVariables(*v, *pv);

    while (tmp != tmp2)
    {
        tmp2 = tmp;
        tmp = (next * tmp).SwapVariables(*v, *pv);

        BDD ntmp = !tmp * reach;
        tmp = bddmgr->bddZero();
        for (set<string>::iterator igs = gi->second.begin(); igs
                != gi->second.end(); igs++)
            tmp += er[*igs] * ntmp;
        tmp *= swapreach;
        tmp = (!Exists(pv, tmp)) * reach;
    }
    //cout << "result in GCK " << i;
    //tmp.print(2,2);
    return tmp;
}

BDD check_nDKH(BDD next, BDD RK, BDD RO)
{
    // Check knowledge assyming correct behaviour
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RO * RK * next * reach); // States from which...
    //result = Exists(a,result*andprot); //Exists a joint action...
    return result;
}

BDD check_ATLX(BDD next, string grpname)
{
    BDD result = bddmgr->bddZero();
    BDD actagtin = bddmgr->bddOne(); // Actions of agents in group
    BDD actagtout = bddmgr->bddOne(); // Actions of agents NOT in group
    int begin, end;

    map<string, set<string> >::iterator gi = is_groups->find(grpname);
    set<string> names_g = gi->second; // the list of agt names in groups

    /*begin = env->get_action_index_begin();
     end = env->get_action_index_end();
     if(names_g.find("Environment")==names_g.end())
     for(int j=begin; j<=end; j++)
     actagtout = actagtout * a[j];
     else
     for(int j=begin; j<=end; j++)
     actagtin = actagtin * a[j];
     */

    for (map<string, basic_agent *>::iterator i = is_agents->begin(); i
            != is_agents->end(); i++)
    {
        begin = i->second->get_action_index_begin();
        end = i->second->get_action_index_end();
        if (names_g.find(i->first) == names_g.end())
        {
            for (int j = begin; j <= end; j++)
            {
                actagtout = actagtout * (*a)[j];
            }
        }
        else
        {
            for (int j = begin; j <= end; j++)
            {
                actagtin = actagtin * (*a)[j];
            }
        }
    }

    BDD * partial = new BDD();

    *partial = (!next) * reach;
    *partial = partial->SwapVariables(*v, *pv);

    for (unsigned int i = 0; i < agents->size(); i++)
        *partial = *partial * (*vevol)[i];

    *partial = Exists(pv, *partial);
    *partial = (*partial) * reach;

    for (unsigned int i = 0; i < agents->size(); i++)
        *partial = *partial * (*vprot)[i];

    *partial = partial->ExistAbstract(actagtout);
    *partial = (!(*partial)) * reach;

    for (unsigned int i = 0; i < agents->size(); i++)
        *partial = *partial * (*vprot)[i];

    *partial = partial->ExistAbstract(actagtout);
    result = partial->ExistAbstract(actagtin) * reach;

    delete (partial);

    return result;
}

BDD check_ATLG(BDD p, string grpname)
{
    BDD tmp = p;
    BDD q = bddmgr->bddOne();
    while (q != tmp)
    {
        q = tmp;
        tmp = p * check_ATLX(tmp, grpname);
    }
    return q;

}

BDD check_ATLU(BDD q1, BDD q2, string grpname)
{
    BDD r = bddmgr->bddZero();
    BDD t = q2;
    while (t != r)
    {
        r = t;
        t = r + check_ATLX(r, grpname) * q1;
    }
    return r;
}

BDD check_EG_fair(BDD p)
{
    // Computes the fixpoint iterating false
    // See "Efficient generation of counterexamples and witnesses in
    // symbolic model checking", Clarke Grumberg McMillan Zhao, 1995
    // Section 4, p.3


    BDD tmp = bddmgr->bddZero();
    BDD q = bddmgr->bddOne();
    BDD fc_bdd = bddmgr->bddOne();
    while (q != tmp)
    {
        tmp = q;
        for (vector<fairness_expression*>::iterator fi = is_fairness->begin(); fi
                != is_fairness->end(); fi++)
        {
            BDD hf = (*fi)->get_bdd_representation(); // The BDD for the fairness constraint
            BDD tmp1 = check_EU(p, q * hf);
            fc_bdd = fc_bdd * check_EX(tmp1);
        }
        q = p * fc_bdd;
    }
    return q;
}

BDD check_EF_fair(BDD p, BDD fair_reach)
{

    return check_EU_fair(reach, p, fair_reach);

}

BDD check_EX_fair(BDD p, BDD fair_reach)
{

    return check_EX(p * fair_reach);
}

BDD check_EU_fair(BDD p, BDD q, BDD fair_reach)
{

    return check_EU(p, q * fair_reach);
}

BDD check_nK_fair(BDD next, BDD RK, BDD fair_reach)
{
    // Used for K and GK and GCK
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RK * next * fair_reach); // States from which...
    //result = Exists(a,result*andprot,bddmgr); //Exists a joint action...
    return result;
}

BDD check_nO_fair(BDD next, BDD RO, BDD fair_reach)
{
    // Check deontic
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RO * next * fair_reach); // States from which...
    //result = Exists(a,result*andprot); //Exists a joint action...
    return result;
}

BDD check_nKH_fair(BDD next, BDD RK, BDD RO, BDD fair_reach)
{
    // Check knowledge assyming correct behaviour
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RO * RK * next * fair_reach); // States from which...
    //result = Exists(a,result*andprot); //Exists a joint action...
    return result;
}

BDD check_GK_fair(BDD next, BDD RK, BDD fair_reach)
{
    //cout << "IN GK" << endl;
    //next.print(2,2);
    //RK.print(2,2);
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RK * !next * fair_reach); // States from which...
    //result = Exists(a,result*andprot); //Exists a joint action...
    result = !result * reach;
    //result.print(2,2);
    return result;
}

BDD check_nGK_fair(BDD next, BDD RK, BDD fair_reach)
{
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RK * next * fair_reach); // States from which...
    return result;
}

BDD check_DK_fair(BDD next, BDD RK, BDD fair_reach)
{
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RK * !next * fair_reach); // States from which...
    //result = Exists(a,result*andprot); //Exists a joint action...
    result = !result * reach;
    return result;
}

BDD check_nDK_fair(BDD next, BDD RK, BDD fair_reach)
{
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RK * next * fair_reach); // States from which...
    return result;
}

BDD check_GCK_fair(BDD next, BDD RK, BDD fair_reach)
{
    // GCK p = GK(p * GCK(p)) see fhmv:rak, section 11.5
    // cout << "In GCK, formula to be checked:" << endl;
    //next.print(2,2);
    //cout << "relation:" << endl;
    //RK.print(2,2);

    BDD tmp = reach;
    BDD tmp2 = next;
    while (tmp != tmp2)
    {
        tmp2 = tmp;
        tmp = check_GK_fair(next * tmp, RK, fair_reach);
    }
    //cout << "result in GCK " << i;
    //tmp.print(2,2);
    return tmp;
}

BDD check_nDKH_fair(BDD next, BDD RK, BDD RO, BDD fair_reach)
{
    // Check knowledge assyming correct behaviour
    next = next.SwapVariables(*v, *pv); // Now it's the next state
    BDD result = Exists(pv, RO * RK * next * fair_reach); // States from which...
    //result = Exists(a,result*andprot); //Exists a joint action...
    return result;
}

BDD get_K_states(BDD aset1, BDD *state, string name)
{
    basic_agent *agent = (*is_agents)[name];
    BDD localstate = agent->project_local_state(state, v);
    return aset1 * localstate;
}

BDD get_nK_states(BDD *state, string name)
{
    basic_agent *agent = (*is_agents)[name];
    BDD localstate = agent->project_local_state(state, v);
    return reach * localstate;
}

BDD get_nK_states_fair(BDD *state, string name, BDD fair_reach)
{
    basic_agent *agent = (*is_agents)[name];
    BDD localstate = agent->project_local_state(state, v);
    return fair_reach * localstate;
}

BDD get_GK_states(BDD aset1, BDD *state, string name)
{
    BDD tmpaset1 = bddmgr->bddZero();
    set<string> names_g = (*is_groups)[name];
    for (set<string>::iterator igs = names_g.begin(); igs != names_g.end(); igs++)
    {
        basic_agent *agent = (*is_agents)[*igs];
        BDD localstate = agent->project_local_state(state, v);
        tmpaset1 = tmpaset1 + (aset1 * localstate);
    }
    return tmpaset1;
}

BDD get_DK_states(BDD aset1, BDD *state, string name)
{
    BDD tmpaset1 = aset1;
    set<string> names_g = (*is_groups)[name];
    for (set<string>::iterator igs = names_g.begin(); igs != names_g.end(); igs++)
    {
        basic_agent *agent = (*is_agents)[*igs];
        BDD localstate = agent->project_local_state(state, v);
        tmpaset1 = tmpaset1 * localstate;
    }
    return tmpaset1;
}

BDD get_agent_greenstates(BDD aset1, string name)
{
    BDD greenstates = deor[name].SwapVariables(*v, *pv);
    return aset1 * greenstates;
}

BDD get_group_greenstates(BDD aset1, string name)
{
    BDD tmpaset1 = aset1;
    set<string> names_g = (*is_groups)[name];
    for (set<string>::iterator igs = names_g.begin(); igs != names_g.end(); igs++)
    {
        BDD greenstates = deor[*igs].SwapVariables(*v, *pv);
        tmpaset1 = tmpaset1 * greenstates;
    }
    return tmpaset1;
}

DdNode * addApplyLT(DdManager* mgr, DdNode ** n1, DdNode ** n2)
{
    DdNode *F, *G;

    F = *n1;
    G = *n2;
    if (F->index == CUDD_CONST_INDEX && G->index == CUDD_CONST_INDEX)
    {
        if (F->type.value < G->type.value)
            return mgr->one;
        else
            return mgr->zero;
    }
    return (NULL);
}

ADD addLT(ADD a1, ADD a2)
{
    DdNode * n1 = a1.getNode();
    DdNode * n2 = a2.getNode();
    DdNode *result = Cudd_addApply(bddmgr->getManager(), &addApplyLT, n1, n2);
    ADD res(bddmgr, result);
    return res;
}

DdNode * addApplyGT(DdManager* mgr, DdNode ** n1, DdNode ** n2)
{
    DdNode *F, *G;

    F = *n1;
    G = *n2;
    if (F->index == CUDD_CONST_INDEX && G->index == CUDD_CONST_INDEX)
    {
        if (F->type.value > G->type.value)
            return mgr->one;
        else
            return mgr->zero;
    }
    return (NULL);
}

ADD addGT(ADD a1, ADD a2)
{
    DdNode * n1 = a1.getNode();
    DdNode * n2 = a2.getNode();
    DdNode *result = Cudd_addApply(bddmgr->getManager(), &addApplyGT, n1, n2);
    ADD res(bddmgr, result);
    return res;
}

DdNode * addApplyEQ(DdManager* mgr, DdNode ** n1, DdNode ** n2)
{
    DdNode *F, *G;

    F = *n1;
    G = *n2;
    if (F->index == CUDD_CONST_INDEX && G->index == CUDD_CONST_INDEX)
    {
        if (F->type.value == G->type.value)
            return mgr->one;
        else
            return mgr->zero;
    }
    return (NULL);
}

ADD addEQ(ADD a1, ADD a2)
{
    DdNode * n1 = a1.getNode();
    DdNode * n2 = a2.getNode();
    DdNode *result = Cudd_addApply(bddmgr->getManager(), &addApplyEQ, n1, n2);
    ADD res(bddmgr, result);
    return res;
}

DdNode * addApplyGE(DdManager* mgr, DdNode ** n1, DdNode ** n2)
{
    DdNode *F, *G;

    F = *n1;
    G = *n2;
    if (F->index == CUDD_CONST_INDEX && G->index == CUDD_CONST_INDEX)
    {
        if (F->type.value >= G->type.value)
            return mgr->one;
        else
            return mgr->zero;
    }
    return (NULL);
}

ADD addGE(ADD a1, ADD a2)
{
    DdNode * n1 = a1.getNode();
    DdNode * n2 = a2.getNode();
    DdNode *result = Cudd_addApply(bddmgr->getManager(), &addApplyGE, n1, n2);
    ADD res(bddmgr, result);
    return res;
}

DdNode * addApplyLE(DdManager* mgr, DdNode ** n1, DdNode ** n2)
{
    DdNode *F, *G;

    F = *n1;
    G = *n2;
    if (F->index == CUDD_CONST_INDEX && G->index == CUDD_CONST_INDEX)
    {
        if (F->type.value <= G->type.value)
            return mgr->one;
        else
            return mgr->zero;
    }
    return (NULL);
}

ADD addLE(ADD a1, ADD a2)
{
    DdNode * n1 = a1.getNode();
    DdNode * n2 = a2.getNode();
    DdNode *result = Cudd_addApply(bddmgr->getManager(), &addApplyLE, n1, n2);
    ADD res(bddmgr, result);
    return res;
}

DdNode * addApplyNEQ(DdManager* mgr, DdNode ** n1, DdNode ** n2)
{
    DdNode *F, *G;

    F = *n1;
    G = *n2;
    if (F->index == CUDD_CONST_INDEX && G->index == CUDD_CONST_INDEX)
    {
        if (F->type.value != G->type.value)
            return mgr->one;
        else
            return mgr->zero;
    }
    return (NULL);
}

ADD addNEQ(ADD a1, ADD a2)
{
    DdNode * n1 = a1.getNode();
    DdNode * n2 = a2.getNode();
    DdNode *result = Cudd_addApply(bddmgr->getManager(), &addApplyNEQ, n1, n2);
    ADD res(bddmgr, result);
    return res;
}

BDD permuteBDDs(int start1, int start2, int length)
{
    BDD permutation = bddmgr->bddOne();
    for (int i = 0; i < length; i++)
        permutation = permutation * ((!(*v)[start1 + i] + (*pv)[start2 + i])
                * ((*v)[start1 + i] + !(*pv)[start2 + i]));
    //if(k > 0)
    for (int i = 0; i < obsvars_bdd_length; i++)
        permutation = permutation * ((!(*v)[i] + (*pv)[i]) * ((*v)[i]
                + !(*pv)[i]));
    return permutation;
}

BDD permuteAgents(int agent1, int agent2)
{
    int start1 = (*agents)[agent1]->get_var_index_begin();
    int end1 = (*agents)[agent1]->get_var_index_end();
    int start2 = (*agents)[agent2]->get_var_index_begin();
    int end2 = (*agents)[agent2]->get_var_index_end();
    int length = (end1 - start1 + 1 > end2 - start2 + 1) ? end2 - start2 + 1
            : end1 - start1 + 1;
    return permuteBDDs(start1, start2, length);
}

BDD permuteAgents(string agentname1, string agentname2)
{
    basic_agent* agent1 = (*is_agents)[agentname1];
    basic_agent* agent2 = (*is_agents)[agentname2];
    int start1 = agent1->get_var_index_begin();
    int end1 = agent1->get_var_index_end();
    int start2 = agent2->get_var_index_begin();
    int end2 = agent2->get_var_index_end();
    int length = (end1 - start1 + 1 > end2 - start2 + 1) ? end2 - start2 + 1
            : end1 - start1 + 1;
    return permuteBDDs(start1, start2, length);
}

string permutation_name(string prefix, map<string, string> *permutation)
{
    string name = prefix;
    for (unsigned int k = 1; k < agents->size(); k++)
    {
        name += "_" + (*permutation)[(*agents)[k]->get_name()];
    }
    return name;
}

vector<map<string, string>*>* compute_round_permutation()
{
    vector<map<string, string>*>* permutations = new vector<
            map<string, string>*> ();
    unsigned int n = (unsigned int) agents->size();
    for (unsigned int i = 0; i < n - 1; i++)
    {
        map<string, string>* permutation = new map<string, string> ();
        (*permutation)["Environment"] = "Environment";
        for (unsigned int j = 1; j < n; j++)
        {
            unsigned int k = (i + j) % n;
            if (k < j)
                k++;
            (*permutation)[(*agents)[j]->get_name()] = (*agents)[k]->get_name();
        }
        permutations->push_back(permutation);
        /*for(unsigned int j=0; j<n; j++) {
         cout << (*agents)[j]->get_name() << ", ";
         }
         cout << endl;
         for(unsigned int j=0; j<n; j++) {
         cout << (*permutation)[(*agents)[j]->get_name()] << ", ";
         }
         cout << endl << endl;*/
    }
    return permutations;
}

void recursively_compute_permutations(
        vector<map<string, string>*> *permutations,
        vector<string> *agent_names, vector<string> *agents_left, map<string,
                string> *permutation)
{
    unsigned int n = (unsigned int) agent_names->size();
    string name = (*agent_names)[0];
    if (n == 1)
    {
        (*permutation)[name] = (*agents_left)[0];
        (*permutation)["Environment"] = "Environment";
        permutations->push_back(permutation);
    }
    else
        for (unsigned int i = 0; i < n; i++)
        {
            map<string, string> *new_permutation = new map<string, string> (
                    *permutation);
            string name1 = (*agents_left)[i];
            (*new_permutation)[name] = name1;
            vector<string>* new_agent_names = new vector<string> (
                    agent_names->begin() + 1, agent_names->end());
            //new_agent_names->erase(new_agent_names->begin());
            vector<string>* new_agents_left = new vector<string> (*agents_left);
            new_agents_left->erase(new_agents_left->begin() + i);
            recursively_compute_permutations(permutations, new_agent_names,
                    new_agents_left, new_permutation);
        }
}

vector<map<string, string>*>* compute_arbitrary_permutation()
{
    vector<map<string, string>*>* permutations = new vector<
            map<string, string>*> ();
    unsigned int n = (unsigned int) agents->size();
    vector<string> *agent_names = new vector<string> ();
    for (unsigned int i = 1; i < n; i++)
        agent_names->push_back((*agents)[i]->get_name());
    vector<string> *agents_left = new vector<string> (*agent_names);
    map<string, string>* permutation = new map<string, string> ();
    recursively_compute_permutations(permutations, agent_names, agents_left,
            permutation);

    /*for(unsigned int j=0; j<(unsigned int)permutations->size(); j++) {
     permutation = (*permutations)[j];
     for(unsigned int j=0; j<n; j++) {
     cout << (*agents)[j]->get_name() << ", ";
     }
     cout << endl;
     for(unsigned int k=0; k<n; k++)
     cout << (*permutation)[(*agents)[k]->get_name()] << ", ";
     cout << endl << endl;
     }
     cout << "number of permutations = " << permutations->size() << endl;*/
    return permutations;
}
